Nuprl Lemma : es-le-before_wf
11,40
postcript
pdf
es
:ES,
e
:E. es-le-before(
es
;
e
)
(E List)
latex
Definitions
E
,
type
List
,
[]
,
t
T
,
A
List
,
s
=
t
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
[
car
/
cdr
]
,
{
x
:
A
|
B
(
x
)}
,
before(
e
)
,
as
@
bs
,
ES
,
es-le-before(
es
;
e
)
Lemmas
event
system
wf
,
append
wf
,
es-before
wf
,
es-E
wf
origin
es:ES, e:E. es-le-before(es;e) 
(E List) es:ES, e:E. es-le-before(es;e) (E List) T
B(x)x:A. B(x)